YES 2.085
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ IFR
mainModule List
| ((delete :: Eq a => [a] -> [[a]] -> [[a]]) :: Eq a => [a] -> [[a]] -> [[a]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| delete :: Eq a => a -> [a] -> [a]
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | _ _ [] | = | [] |
deleteBy | eq x (y : ys) | = | if x `eq` y then ys else y : deleteBy eq x ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
If Reductions:
The following If expression
if eq x y then ys else y : deleteBy eq x ys
is transformed to
deleteBy0 | ys y eq x True | = ys |
deleteBy0 | ys y eq x False | = y : deleteBy eq x ys |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
mainModule List
| ((delete :: Eq a => [a] -> [[a]] -> [[a]]) :: Eq a => [a] -> [[a]] -> [[a]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| delete :: Eq a => a -> [a] -> [a]
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | _ _ [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((delete :: Eq a => [a] -> [[a]] -> [[a]]) :: Eq a => [a] -> [[a]] -> [[a]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| delete :: Eq a => a -> [a] -> [a]
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | vw vx [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule List
| (delete :: Eq a => [a] -> [[a]] -> [[a]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| delete :: Eq a => a -> [a] -> [a]
|
| deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]
deleteBy | vw vx [] | = | [] |
deleteBy | eq x (y : ys) | = | deleteBy0 ys y eq x (x `eq` y) |
|
|
deleteBy0 | ys y eq x True | = | ys |
deleteBy0 | ys y eq x False | = | y : deleteBy eq x ys |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xy3200), Succ(xy4001000)) → new_primPlusNat(xy3200, xy4001000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xy3200), Succ(xy4001000)) → new_primPlusNat(xy3200, xy4001000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xy30100), Succ(xy400100)) → new_primMulNat(xy30100, Succ(xy400100))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xy30100), Succ(xy400100)) → new_primMulNat(xy30100, Succ(xy400100))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xy3000), Succ(xy40000)) → new_primEqNat(xy3000, xy40000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xy3000), Succ(xy40000)) → new_primEqNat(xy3000, xy40000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(ty_@2, bbf), bbg), ca) → new_esEs1(xy301, xy4001, bbf, bbg)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(ty_Maybe, bbh), ca) → new_esEs2(xy301, xy4001, bbh)
new_esEs0(Left(xy300), Left(xy4000), app(ty_[], cc), bc) → new_esEs(xy300, xy4000, cc)
new_esEs2(Just(xy300), Just(xy4000), app(ty_[], ha)) → new_esEs(xy300, xy4000, ha)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(app(ty_@3, gf), gg), gh)) → new_esEs3(xy301, xy4001, gf, gg, gh)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xy302, xy4002, bdb, bdc, bdd)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(ty_[], bcd)) → new_esEs(xy302, xy4002, bcd)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_Either, eg), eh), be) → new_esEs0(xy300, xy4000, eg, eh)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(ty_Either, ga), gb)) → new_esEs0(xy301, xy4001, ga, gb)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bae), baf), bh, ca) → new_esEs1(xy300, xy4000, bae, baf)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xy310, xy4010, bg, bh, ca)
new_esEs0(Right(xy300), Right(xy4000), bb, app(app(ty_@2, dh), ea)) → new_esEs1(xy300, xy4000, dh, ea)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_[], bab), bh, ca) → new_esEs(xy300, xy4000, bab)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(ty_[], bbc), ca) → new_esEs(xy301, xy4001, bbc)
new_esEs0(Left(xy300), Left(xy4000), app(app(app(ty_@3, db), dc), dd), bc) → new_esEs3(xy300, xy4000, db, dc, dd)
new_esEs2(Just(xy300), Just(xy4000), app(ty_Maybe, hf)) → new_esEs2(xy300, xy4000, hf)
new_esEs0(Left(xy300), Left(xy4000), app(app(ty_Either, cd), ce), bc) → new_esEs0(xy300, xy4000, cd, ce)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_@2, hd), he)) → new_esEs1(xy300, xy4000, hd, he)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(ty_[], fh)) → new_esEs(xy301, xy4001, fh)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_Maybe, bf)) → new_esEs2(xy310, xy4010, bf)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_Maybe, fc), be) → new_esEs2(xy300, xy4000, fc)
new_esEs0(Right(xy300), Right(xy4000), bb, app(app(app(ty_@3, ec), ed), ee)) → new_esEs3(xy300, xy4000, ec, ed, ee)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_[], ef), be) → new_esEs(xy300, xy4000, ef)
new_esEs0(Right(xy300), Right(xy4000), bb, app(app(ty_Either, df), dg)) → new_esEs0(xy300, xy4000, df, dg)
new_esEs0(Left(xy300), Left(xy4000), app(ty_Maybe, da), bc) → new_esEs2(xy300, xy4000, da)
new_esEs0(Right(xy300), Right(xy4000), bb, app(ty_Maybe, eb)) → new_esEs2(xy300, xy4000, eb)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(ty_@2, gc), gd)) → new_esEs1(xy301, xy4001, gc, gd)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_@2, bd), be)) → new_esEs1(xy310, xy4010, bd, be)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(app(ty_@3, bca), bcb), bcc), ca) → new_esEs3(xy301, xy4001, bca, bcb, bcc)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_Either, bb), bc)) → new_esEs0(xy310, xy4010, bb, bc)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), cb) → new_esEs(xy311, xy4011, cb)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(ty_@2, bcg), bch)) → new_esEs1(xy302, xy4002, bcg, bch)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(app(ty_@3, fd), ff), fg), be) → new_esEs3(xy300, xy4000, fd, ff, fg)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_@2, fa), fb), be) → new_esEs1(xy300, xy4000, fa, fb)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bag), bh, ca) → new_esEs2(xy300, xy4000, bag)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(ty_Maybe, bda)) → new_esEs2(xy302, xy4002, bda)
new_esEs0(Right(xy300), Right(xy4000), bb, app(ty_[], de)) → new_esEs(xy300, xy4000, de)
new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(ty_Maybe, ge)) → new_esEs2(xy301, xy4001, ge)
new_esEs2(Just(xy300), Just(xy4000), app(app(ty_Either, hb), hc)) → new_esEs0(xy300, xy4000, hb, hc)
new_esEs2(Just(xy300), Just(xy4000), app(app(app(ty_@3, hg), hh), baa)) → new_esEs3(xy300, xy4000, hg, hh, baa)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(ty_Either, bbd), bbe), ca) → new_esEs0(xy301, xy4001, bbd, bbe)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(ty_Either, bce), bcf)) → new_esEs0(xy302, xy4002, bce, bcf)
new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_[], ba)) → new_esEs(xy310, xy4010, ba)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bah), bba), bbb), bh, ca) → new_esEs3(xy300, xy4000, bah, bba, bbb)
new_esEs0(Left(xy300), Left(xy4000), app(app(ty_@2, cf), cg), bc) → new_esEs1(xy300, xy4000, cf, cg)
new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bac), bad), bh, ca) → new_esEs0(xy300, xy4000, bac, bad)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(xy300), Just(xy4000), app(app(app(ty_@3, hg), hh), baa)) → new_esEs3(xy300, xy4000, hg, hh, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(xy300), Just(xy4000), app(app(ty_Either, hb), hc)) → new_esEs0(xy300, xy4000, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(xy310, xy4010, bg, bh, ca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_Either, bb), bc)) → new_esEs0(xy310, xy4010, bb, bc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy4000), app(ty_Maybe, hf)) → new_esEs2(xy300, xy4000, hf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_Maybe, bf)) → new_esEs2(xy310, xy4010, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(xy300), Just(xy4000), app(app(ty_@2, hd), he)) → new_esEs1(xy300, xy4000, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(xy300), Just(xy4000), app(ty_[], ha)) → new_esEs(xy300, xy4000, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(app(ty_@2, bd), be)) → new_esEs1(xy310, xy4010, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(app(ty_@3, gf), gg), gh)) → new_esEs3(xy301, xy4001, gf, gg, gh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(app(ty_@3, fd), ff), fg), be) → new_esEs3(xy300, xy4000, fd, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xy302, xy4002, bdb, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(app(ty_@3, bca), bcb), bcc), ca) → new_esEs3(xy301, xy4001, bca, bcb, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(app(ty_@3, bah), bba), bbb), bh, ca) → new_esEs3(xy300, xy4000, bah, bba, bbb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Left(xy300), Left(xy4000), app(app(app(ty_@3, db), dc), dd), bc) → new_esEs3(xy300, xy4000, db, dc, dd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(Right(xy300), Right(xy4000), bb, app(app(app(ty_@3, ec), ed), ee)) → new_esEs3(xy300, xy4000, ec, ed, ee)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_Either, eg), eh), be) → new_esEs0(xy300, xy4000, eg, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(ty_Either, ga), gb)) → new_esEs0(xy301, xy4001, ga, gb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_Maybe, fc), be) → new_esEs2(xy300, xy4000, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(ty_Maybe, ge)) → new_esEs2(xy301, xy4001, ge)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(app(ty_@2, gc), gd)) → new_esEs1(xy301, xy4001, gc, gd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(app(ty_@2, fa), fb), be) → new_esEs1(xy300, xy4000, fa, fb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), bd, app(ty_[], fh)) → new_esEs(xy301, xy4001, fh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xy300, xy301), @2(xy4000, xy4001), app(ty_[], ef), be) → new_esEs(xy300, xy4000, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), cb) → new_esEs(xy311, xy4011, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(:(xy310, xy311), :(xy4010, xy4011), app(ty_[], ba)) → new_esEs(xy310, xy4010, ba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(ty_Either, bbd), bbe), ca) → new_esEs0(xy301, xy4001, bbd, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(ty_Either, bce), bcf)) → new_esEs0(xy302, xy4002, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_Either, bac), bad), bh, ca) → new_esEs0(xy300, xy4000, bac, bad)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(app(ty_Either, cd), ce), bc) → new_esEs0(xy300, xy4000, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Right(xy300), Right(xy4000), bb, app(app(ty_Either, df), dg)) → new_esEs0(xy300, xy4000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(ty_Maybe, bbh), ca) → new_esEs2(xy301, xy4001, bbh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(ty_Maybe, bda)) → new_esEs2(xy302, xy4002, bda)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_Maybe, bag), bh, ca) → new_esEs2(xy300, xy4000, bag)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Left(xy300), Left(xy4000), app(ty_Maybe, da), bc) → new_esEs2(xy300, xy4000, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy300), Right(xy4000), bb, app(ty_Maybe, eb)) → new_esEs2(xy300, xy4000, eb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(app(ty_@2, bbf), bbg), ca) → new_esEs1(xy301, xy4001, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(app(ty_@2, bae), baf), bh, ca) → new_esEs1(xy300, xy4000, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(app(ty_@2, bcg), bch)) → new_esEs1(xy302, xy4002, bcg, bch)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, bh, app(ty_[], bcd)) → new_esEs(xy302, xy4002, bcd)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), app(ty_[], bab), bh, ca) → new_esEs(xy300, xy4000, bab)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), bg, app(ty_[], bbc), ca) → new_esEs(xy301, xy4001, bbc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs0(Right(xy300), Right(xy4000), bb, app(app(ty_@2, dh), ea)) → new_esEs1(xy300, xy4000, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(app(ty_@2, cf), cg), bc) → new_esEs1(xy300, xy4000, cf, cg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(Left(xy300), Left(xy4000), app(ty_[], cc), bc) → new_esEs(xy300, xy4000, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(Right(xy300), Right(xy4000), bb, app(ty_[], de)) → new_esEs(xy300, xy4000, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(xy400, xy401), xy41), bb) → new_deleteBy([], xy41, bb)
new_deleteBy0(xy12, xy13, xy14, xy15, xy16, False, ba) → new_deleteBy(:(xy15, xy16), xy12, ba)
new_deleteBy(:(xy30, xy31), :([], xy41), bb) → new_deleteBy(:(xy30, xy31), xy41, bb)
new_deleteBy(:(xy30, xy31), :(:(xy400, xy401), xy41), bb) → new_deleteBy0(xy41, xy400, xy401, xy30, xy31, new_asAs(new_esEs4(xy30, xy400, bb), new_esEs5(xy31, xy401, bb)), bb)
The TRS R consists of the following rules:
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Maybe, bh)) → new_esEs16(xy310, xy4010, bh)
new_esEs6(xy310, xy4010, ty_Integer) → new_esEs10(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Maybe, bch), be) → new_esEs16(xy300, xy4000, bch)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Float) → new_esEs7(xy300, xy4000)
new_primPlusNat1(Succ(xy3200), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy3200, xy4001000)))
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, cf), cg)) → new_esEs13(xy300, xy4000, cf, cg)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs21(xy301, xy4001, app(ty_Maybe, fh)) → new_esEs16(xy301, xy4001, fh)
new_esEs20(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Float) → new_esEs7(xy310, xy4010)
new_esEs24(xy302, xy4002, ty_Char) → new_esEs9(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs5([], [], bb) → True
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Ratio, bec)) → new_esEs17(xy300, xy4000, bec)
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), be) → new_esEs13(xy300, xy4000, bcd, bce)
new_esEs23(xy301, xy4001, app(app(ty_Either, hh), baa)) → new_esEs13(xy301, xy4001, hh, baa)
new_esEs6(xy310, xy4010, ty_Int) → new_esEs11(xy310, xy4010)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_[], bde)) → new_esEs5(xy300, xy4000, bde)
new_esEs24(xy302, xy4002, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs18(xy302, xy4002, bbh, bca, bcb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(:(xy310, xy311), :(xy4010, xy4011), bb) → new_asAs(new_esEs6(xy310, xy4010, bb), new_esEs5(xy311, xy4011, bb))
new_esEs16(Nothing, Nothing, bh) → True
new_esEs21(xy301, xy4001, app(ty_[], fb)) → new_esEs5(xy301, xy4001, fb)
new_esEs11(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_@2, bdh), bea)) → new_esEs14(xy300, xy4000, bdh, bea)
new_esEs6(xy310, xy4010, ty_Ordering) → new_esEs8(xy310, xy4010)
new_esEs5([], :(xy4010, xy4011), bb) → False
new_esEs5(:(xy310, xy311), [], bb) → False
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs8(xy30, xy400)
new_esEs6(xy310, xy4010, app(app(ty_@2, bf), bg)) → new_esEs14(xy310, xy4010, bf, bg)
new_esEs22(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs20(xy300, xy4000, app(app(ty_@2, ec), ed)) → new_esEs14(xy300, xy4000, ec, ed)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs20(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Maybe, ee)) → new_esEs16(xy300, xy4000, ee)
new_esEs13(Left(xy300), Left(xy4000), ty_Ordering, be) → new_esEs8(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_@0, be) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(ty_Either, bd), be)) → new_esEs13(xy310, xy4010, bd, be)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, dc)) → new_esEs16(xy300, xy4000, dc)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(app(ty_@3, bed), bee), bef)) → new_esEs18(xy300, xy4000, bed, bee, bef)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_Char, be) → new_esEs9(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, de), df), dg)) → new_esEs18(xy300, xy4000, de, df, dg)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs20(xy300, xy4000, app(app(ty_Either, ea), eb)) → new_esEs13(xy300, xy4000, ea, eb)
new_esEs12(@0, @0) → True
new_esEs6(xy310, xy4010, ty_Double) → new_esEs19(xy310, xy4010)
new_esEs22(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs13(xy300, xy4000, gf, gg)
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy30, xy400, cb, cc, cd)
new_esEs24(xy302, xy4002, ty_Bool) → new_esEs15(xy302, xy4002)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_[], bc)) → new_esEs5(xy30, xy400, bc)
new_esEs23(xy301, xy4001, app(app(app(ty_@3, baf), bag), bah)) → new_esEs18(xy301, xy4001, baf, bag, bah)
new_esEs20(xy300, xy4000, app(ty_[], dh)) → new_esEs5(xy300, xy4000, dh)
new_esEs22(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs14(xy300, xy4000, gh, ha)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), be) → new_esEs14(xy300, xy4000, bcf, bcg)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(ty_@2, ff), fg)) → new_esEs14(xy301, xy4001, ff, fg)
new_esEs10(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs15(False, True) → False
new_esEs15(True, False) → False
new_esEs23(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs14(@2(xy300, xy301), @2(xy4000, xy4001), bf, bg) → new_asAs(new_esEs20(xy300, xy4000, bf), new_esEs21(xy301, xy4001, bg))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs24(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs24(xy302, xy4002, app(app(ty_@2, bbd), bbe)) → new_esEs14(xy302, xy4002, bbd, bbe)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_[], hg)) → new_esEs5(xy301, xy4001, hg)
new_esEs4(xy30, xy400, ty_Char) → new_esEs9(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_Ratio, bae)) → new_esEs17(xy301, xy4001, bae)
new_esEs22(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Ratio, ef)) → new_esEs17(xy300, xy4000, ef)
new_esEs13(Left(xy300), Left(xy4000), ty_Double, be) → new_esEs19(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs11(xy30, xy400)
new_esEs24(xy302, xy4002, ty_Int) → new_esEs11(xy302, xy4002)
new_esEs22(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_Ratio, ca)) → new_esEs17(xy30, xy400, ca)
new_esEs4(xy30, xy400, ty_Float) → new_esEs7(xy30, xy400)
new_esEs20(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs21(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), be) → new_esEs18(xy300, xy4000, bdb, bdc, bdd)
new_esEs22(xy300, xy4000, app(ty_[], ge)) → new_esEs5(xy300, xy4000, ge)
new_esEs8(LT, LT) → True
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(app(ty_@3, gb), gc), gd)) → new_esEs18(xy301, xy4001, gb, gc, gd)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_asAs(False, xy31) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs8(xy300, xy4000)
new_primEqNat0(Zero, Zero) → True
new_esEs20(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), ty_Integer, be) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_@0) → new_esEs12(xy310, xy4010)
new_esEs18(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cb, cc, cd) → new_asAs(new_esEs22(xy300, xy4000, cb), new_asAs(new_esEs23(xy301, xy4001, cc), new_esEs24(xy302, xy4002, cd)))
new_esEs24(xy302, xy4002, app(ty_Ratio, bbg)) → new_esEs17(xy302, xy4002, bbg)
new_esEs24(xy302, xy4002, app(ty_Maybe, bbf)) → new_esEs16(xy302, xy4002, bbf)
new_esEs13(Left(xy300), Left(xy4000), ty_Int, be) → new_esEs11(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Ratio, ca)) → new_esEs17(xy310, xy4010, ca)
new_esEs6(xy310, xy4010, ty_Bool) → new_esEs15(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_[], bcc), be) → new_esEs5(xy300, xy4000, bcc)
new_esEs23(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs4(xy30, xy400, ty_@0) → new_esEs12(xy30, xy400)
new_esEs8(GT, GT) → True
new_esEs24(xy302, xy4002, app(ty_[], bba)) → new_esEs5(xy302, xy4002, bba)
new_primPlusNat0(Succ(xy320), xy400100) → Succ(Succ(new_primPlusNat1(xy320, xy400100)))
new_esEs24(xy302, xy4002, ty_Integer) → new_esEs10(xy302, xy4002)
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Maybe, beb)) → new_esEs16(xy300, xy4000, beb)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs23(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs10(xy30, xy400)
new_esEs22(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Char) → new_esEs9(xy310, xy4010)
new_esEs23(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Left(xy4000), bd, be) → False
new_esEs13(Left(xy300), Right(xy4000), bd, be) → False
new_esEs15(True, True) → True
new_esEs20(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_Either, bdf), bdg)) → new_esEs13(xy300, xy4000, bdf, bdg)
new_esEs23(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy3200), Zero) → Succ(xy3200)
new_esEs23(xy301, xy4001, app(ty_Maybe, bad)) → new_esEs16(xy301, xy4001, bad)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs21(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, da), db)) → new_esEs14(xy300, xy4000, da, db)
new_esEs7(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(xy30, xy400, app(app(ty_Either, bd), be)) → new_esEs13(xy30, xy400, bd, be)
new_esEs16(Nothing, Just(xy4000), bh) → False
new_esEs16(Just(xy300), Nothing, bh) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs13(Left(xy300), Left(xy4000), ty_Bool, be) → new_esEs15(xy300, xy4000)
new_esEs8(EQ, EQ) → True
new_esEs20(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs24(xy302, xy4002, app(app(ty_Either, bbb), bbc)) → new_esEs13(xy302, xy4002, bbb, bbc)
new_esEs22(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs17(xy300, xy4000, hc)
new_esEs9(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs11(xy300, xy4000)
new_esEs21(xy301, xy4001, app(app(ty_Either, fc), fd)) → new_esEs13(xy301, xy4001, fc, fd)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], ce)) → new_esEs5(xy300, xy4000, ce)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs20(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, app(ty_Ratio, ga)) → new_esEs17(xy301, xy4001, ga)
new_asAs(True, xy31) → xy31
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs22(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs16(xy300, xy4000, hb)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Ratio, bda), be) → new_esEs17(xy300, xy4000, bda)
new_esEs22(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs20(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy310, xy4010, cb, cc, cd)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, bh)) → new_esEs16(xy30, xy400, bh)
new_esEs6(xy310, xy4010, app(ty_[], bc)) → new_esEs5(xy310, xy4010, bc)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, dd)) → new_esEs17(xy300, xy4000, dd)
new_esEs23(xy301, xy4001, app(app(ty_@2, bab), bac)) → new_esEs14(xy301, xy4001, bab, bac)
new_esEs24(xy302, xy4002, ty_Ordering) → new_esEs8(xy302, xy4002)
new_esEs24(xy302, xy4002, ty_Float) → new_esEs7(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_esEs21(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_@2, bf), bg)) → new_esEs14(xy30, xy400, bf, bg)
new_esEs13(Left(xy300), Left(xy4000), ty_Float, be) → new_esEs7(xy300, xy4000)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs17(:%(xy300, xy301), :%(xy4000, xy4001), ca) → new_asAs(new_esEs25(xy300, xy4000, ca), new_esEs26(xy301, xy4001, ca))
new_esEs24(xy302, xy4002, ty_@0) → new_esEs12(xy302, xy4002)
new_esEs21(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs21(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs22(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs18(xy300, xy4000, hd, he, hf)
new_esEs20(xy300, xy4000, app(app(app(ty_@3, eg), eh), fa)) → new_esEs18(xy300, xy4000, eg, eh, fa)
new_esEs15(False, False) → True
The set Q consists of the following terms:
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5([], [], x0)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Double)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(False, True)
new_esEs15(True, False)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(True, True)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(Just(x0), Nothing, x1)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(False, False)
new_esEs8(GT, GT)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs7(Float(x0, x1), Float(x2, x3))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(LT, LT)
new_esEs22(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs10(Integer(x0), Integer(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs6(x0, x1, ty_Int)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs6(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Float)
new_esEs16(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_asAs(True, x0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs6(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs6(x0, x1, ty_Char)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(:(x0, x1), [], x2)
new_esEs6(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs17(:%(x0, x1), :%(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_Char)
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy0(xy12, xy13, xy14, xy15, xy16, False, ba) → new_deleteBy(:(xy15, xy16), xy12, ba)
new_deleteBy(:(xy30, xy31), :([], xy41), bb) → new_deleteBy(:(xy30, xy31), xy41, bb)
new_deleteBy(:(xy30, xy31), :(:(xy400, xy401), xy41), bb) → new_deleteBy0(xy41, xy400, xy401, xy30, xy31, new_asAs(new_esEs4(xy30, xy400, bb), new_esEs5(xy31, xy401, bb)), bb)
The TRS R consists of the following rules:
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Maybe, bh)) → new_esEs16(xy310, xy4010, bh)
new_esEs6(xy310, xy4010, ty_Integer) → new_esEs10(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Maybe, bch), be) → new_esEs16(xy300, xy4000, bch)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Float) → new_esEs7(xy300, xy4000)
new_primPlusNat1(Succ(xy3200), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy3200, xy4001000)))
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, cf), cg)) → new_esEs13(xy300, xy4000, cf, cg)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs21(xy301, xy4001, app(ty_Maybe, fh)) → new_esEs16(xy301, xy4001, fh)
new_esEs20(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Float) → new_esEs7(xy310, xy4010)
new_esEs24(xy302, xy4002, ty_Char) → new_esEs9(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs5([], [], bb) → True
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Ratio, bec)) → new_esEs17(xy300, xy4000, bec)
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), be) → new_esEs13(xy300, xy4000, bcd, bce)
new_esEs23(xy301, xy4001, app(app(ty_Either, hh), baa)) → new_esEs13(xy301, xy4001, hh, baa)
new_esEs6(xy310, xy4010, ty_Int) → new_esEs11(xy310, xy4010)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_[], bde)) → new_esEs5(xy300, xy4000, bde)
new_esEs24(xy302, xy4002, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs18(xy302, xy4002, bbh, bca, bcb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(:(xy310, xy311), :(xy4010, xy4011), bb) → new_asAs(new_esEs6(xy310, xy4010, bb), new_esEs5(xy311, xy4011, bb))
new_esEs16(Nothing, Nothing, bh) → True
new_esEs21(xy301, xy4001, app(ty_[], fb)) → new_esEs5(xy301, xy4001, fb)
new_esEs11(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_@2, bdh), bea)) → new_esEs14(xy300, xy4000, bdh, bea)
new_esEs6(xy310, xy4010, ty_Ordering) → new_esEs8(xy310, xy4010)
new_esEs5([], :(xy4010, xy4011), bb) → False
new_esEs5(:(xy310, xy311), [], bb) → False
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs8(xy30, xy400)
new_esEs6(xy310, xy4010, app(app(ty_@2, bf), bg)) → new_esEs14(xy310, xy4010, bf, bg)
new_esEs22(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs20(xy300, xy4000, app(app(ty_@2, ec), ed)) → new_esEs14(xy300, xy4000, ec, ed)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs20(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Maybe, ee)) → new_esEs16(xy300, xy4000, ee)
new_esEs13(Left(xy300), Left(xy4000), ty_Ordering, be) → new_esEs8(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_@0, be) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(ty_Either, bd), be)) → new_esEs13(xy310, xy4010, bd, be)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, dc)) → new_esEs16(xy300, xy4000, dc)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(app(ty_@3, bed), bee), bef)) → new_esEs18(xy300, xy4000, bed, bee, bef)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_Char, be) → new_esEs9(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, de), df), dg)) → new_esEs18(xy300, xy4000, de, df, dg)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs20(xy300, xy4000, app(app(ty_Either, ea), eb)) → new_esEs13(xy300, xy4000, ea, eb)
new_esEs12(@0, @0) → True
new_esEs6(xy310, xy4010, ty_Double) → new_esEs19(xy310, xy4010)
new_esEs22(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs13(xy300, xy4000, gf, gg)
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy30, xy400, cb, cc, cd)
new_esEs24(xy302, xy4002, ty_Bool) → new_esEs15(xy302, xy4002)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_[], bc)) → new_esEs5(xy30, xy400, bc)
new_esEs23(xy301, xy4001, app(app(app(ty_@3, baf), bag), bah)) → new_esEs18(xy301, xy4001, baf, bag, bah)
new_esEs20(xy300, xy4000, app(ty_[], dh)) → new_esEs5(xy300, xy4000, dh)
new_esEs22(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs14(xy300, xy4000, gh, ha)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), be) → new_esEs14(xy300, xy4000, bcf, bcg)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(ty_@2, ff), fg)) → new_esEs14(xy301, xy4001, ff, fg)
new_esEs10(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs15(False, True) → False
new_esEs15(True, False) → False
new_esEs23(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs14(@2(xy300, xy301), @2(xy4000, xy4001), bf, bg) → new_asAs(new_esEs20(xy300, xy4000, bf), new_esEs21(xy301, xy4001, bg))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs24(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs24(xy302, xy4002, app(app(ty_@2, bbd), bbe)) → new_esEs14(xy302, xy4002, bbd, bbe)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_[], hg)) → new_esEs5(xy301, xy4001, hg)
new_esEs4(xy30, xy400, ty_Char) → new_esEs9(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_Ratio, bae)) → new_esEs17(xy301, xy4001, bae)
new_esEs22(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Ratio, ef)) → new_esEs17(xy300, xy4000, ef)
new_esEs13(Left(xy300), Left(xy4000), ty_Double, be) → new_esEs19(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs11(xy30, xy400)
new_esEs24(xy302, xy4002, ty_Int) → new_esEs11(xy302, xy4002)
new_esEs22(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_Ratio, ca)) → new_esEs17(xy30, xy400, ca)
new_esEs4(xy30, xy400, ty_Float) → new_esEs7(xy30, xy400)
new_esEs20(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs21(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), be) → new_esEs18(xy300, xy4000, bdb, bdc, bdd)
new_esEs22(xy300, xy4000, app(ty_[], ge)) → new_esEs5(xy300, xy4000, ge)
new_esEs8(LT, LT) → True
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(app(ty_@3, gb), gc), gd)) → new_esEs18(xy301, xy4001, gb, gc, gd)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_asAs(False, xy31) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs8(xy300, xy4000)
new_primEqNat0(Zero, Zero) → True
new_esEs20(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), ty_Integer, be) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_@0) → new_esEs12(xy310, xy4010)
new_esEs18(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cb, cc, cd) → new_asAs(new_esEs22(xy300, xy4000, cb), new_asAs(new_esEs23(xy301, xy4001, cc), new_esEs24(xy302, xy4002, cd)))
new_esEs24(xy302, xy4002, app(ty_Ratio, bbg)) → new_esEs17(xy302, xy4002, bbg)
new_esEs24(xy302, xy4002, app(ty_Maybe, bbf)) → new_esEs16(xy302, xy4002, bbf)
new_esEs13(Left(xy300), Left(xy4000), ty_Int, be) → new_esEs11(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Ratio, ca)) → new_esEs17(xy310, xy4010, ca)
new_esEs6(xy310, xy4010, ty_Bool) → new_esEs15(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_[], bcc), be) → new_esEs5(xy300, xy4000, bcc)
new_esEs23(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs4(xy30, xy400, ty_@0) → new_esEs12(xy30, xy400)
new_esEs8(GT, GT) → True
new_esEs24(xy302, xy4002, app(ty_[], bba)) → new_esEs5(xy302, xy4002, bba)
new_primPlusNat0(Succ(xy320), xy400100) → Succ(Succ(new_primPlusNat1(xy320, xy400100)))
new_esEs24(xy302, xy4002, ty_Integer) → new_esEs10(xy302, xy4002)
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Maybe, beb)) → new_esEs16(xy300, xy4000, beb)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs23(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs10(xy30, xy400)
new_esEs22(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Char) → new_esEs9(xy310, xy4010)
new_esEs23(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Left(xy4000), bd, be) → False
new_esEs13(Left(xy300), Right(xy4000), bd, be) → False
new_esEs15(True, True) → True
new_esEs20(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_Either, bdf), bdg)) → new_esEs13(xy300, xy4000, bdf, bdg)
new_esEs23(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy3200), Zero) → Succ(xy3200)
new_esEs23(xy301, xy4001, app(ty_Maybe, bad)) → new_esEs16(xy301, xy4001, bad)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs21(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, da), db)) → new_esEs14(xy300, xy4000, da, db)
new_esEs7(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(xy30, xy400, app(app(ty_Either, bd), be)) → new_esEs13(xy30, xy400, bd, be)
new_esEs16(Nothing, Just(xy4000), bh) → False
new_esEs16(Just(xy300), Nothing, bh) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs13(Left(xy300), Left(xy4000), ty_Bool, be) → new_esEs15(xy300, xy4000)
new_esEs8(EQ, EQ) → True
new_esEs20(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs24(xy302, xy4002, app(app(ty_Either, bbb), bbc)) → new_esEs13(xy302, xy4002, bbb, bbc)
new_esEs22(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs17(xy300, xy4000, hc)
new_esEs9(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs11(xy300, xy4000)
new_esEs21(xy301, xy4001, app(app(ty_Either, fc), fd)) → new_esEs13(xy301, xy4001, fc, fd)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], ce)) → new_esEs5(xy300, xy4000, ce)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs20(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, app(ty_Ratio, ga)) → new_esEs17(xy301, xy4001, ga)
new_asAs(True, xy31) → xy31
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs22(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs16(xy300, xy4000, hb)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Ratio, bda), be) → new_esEs17(xy300, xy4000, bda)
new_esEs22(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs20(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy310, xy4010, cb, cc, cd)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, bh)) → new_esEs16(xy30, xy400, bh)
new_esEs6(xy310, xy4010, app(ty_[], bc)) → new_esEs5(xy310, xy4010, bc)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, dd)) → new_esEs17(xy300, xy4000, dd)
new_esEs23(xy301, xy4001, app(app(ty_@2, bab), bac)) → new_esEs14(xy301, xy4001, bab, bac)
new_esEs24(xy302, xy4002, ty_Ordering) → new_esEs8(xy302, xy4002)
new_esEs24(xy302, xy4002, ty_Float) → new_esEs7(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_esEs21(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_@2, bf), bg)) → new_esEs14(xy30, xy400, bf, bg)
new_esEs13(Left(xy300), Left(xy4000), ty_Float, be) → new_esEs7(xy300, xy4000)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs17(:%(xy300, xy301), :%(xy4000, xy4001), ca) → new_asAs(new_esEs25(xy300, xy4000, ca), new_esEs26(xy301, xy4001, ca))
new_esEs24(xy302, xy4002, ty_@0) → new_esEs12(xy302, xy4002)
new_esEs21(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs21(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs22(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs18(xy300, xy4000, hd, he, hf)
new_esEs20(xy300, xy4000, app(app(app(ty_@3, eg), eh), fa)) → new_esEs18(xy300, xy4000, eg, eh, fa)
new_esEs15(False, False) → True
The set Q consists of the following terms:
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5([], [], x0)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Double)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(False, True)
new_esEs15(True, False)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(True, True)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(Just(x0), Nothing, x1)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(False, False)
new_esEs8(GT, GT)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs7(Float(x0, x1), Float(x2, x3))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(LT, LT)
new_esEs22(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs10(Integer(x0), Integer(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs6(x0, x1, ty_Int)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs6(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Float)
new_esEs16(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_asAs(True, x0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs6(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs6(x0, x1, ty_Char)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(:(x0, x1), [], x2)
new_esEs6(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs17(:%(x0, x1), :%(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_Char)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy(:(xy30, xy31), :([], xy41), bb) → new_deleteBy(:(xy30, xy31), xy41, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
- new_deleteBy(:(xy30, xy31), :(:(xy400, xy401), xy41), bb) → new_deleteBy0(xy41, xy400, xy401, xy30, xy31, new_asAs(new_esEs4(xy30, xy400, bb), new_esEs5(xy31, xy401, bb)), bb)
The graph contains the following edges 2 > 1, 2 > 2, 2 > 3, 1 > 4, 1 > 5, 3 >= 7
- new_deleteBy0(xy12, xy13, xy14, xy15, xy16, False, ba) → new_deleteBy(:(xy15, xy16), xy12, ba)
The graph contains the following edges 1 >= 2, 7 >= 3
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(xy400, xy401), xy41), bb) → new_deleteBy([], xy41, bb)
The TRS R consists of the following rules:
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Maybe, bh)) → new_esEs16(xy310, xy4010, bh)
new_esEs6(xy310, xy4010, ty_Integer) → new_esEs10(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Maybe, bch), be) → new_esEs16(xy300, xy4000, bch)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Float) → new_esEs7(xy300, xy4000)
new_primPlusNat1(Succ(xy3200), Succ(xy4001000)) → Succ(Succ(new_primPlusNat1(xy3200, xy4001000)))
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_Either, cf), cg)) → new_esEs13(xy300, xy4000, cf, cg)
new_primEqInt(Neg(Succ(xy3000)), Pos(xy4000)) → False
new_primEqInt(Pos(Succ(xy3000)), Neg(xy4000)) → False
new_esEs21(xy301, xy4001, app(ty_Maybe, fh)) → new_esEs16(xy301, xy4001, fh)
new_esEs20(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Float) → new_esEs7(xy310, xy4010)
new_esEs24(xy302, xy4002, ty_Char) → new_esEs9(xy302, xy4002)
new_primEqInt(Neg(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(xy40000))) → False
new_esEs5([], [], bb) → True
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Ratio, bec)) → new_esEs17(xy300, xy4000, bec)
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_Either, bcd), bce), be) → new_esEs13(xy300, xy4000, bcd, bce)
new_esEs23(xy301, xy4001, app(app(ty_Either, hh), baa)) → new_esEs13(xy301, xy4001, hh, baa)
new_esEs6(xy310, xy4010, ty_Int) → new_esEs11(xy310, xy4010)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_[], bde)) → new_esEs5(xy300, xy4000, bde)
new_esEs24(xy302, xy4002, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs18(xy302, xy4002, bbh, bca, bcb)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(:(xy310, xy311), :(xy4010, xy4011), bb) → new_asAs(new_esEs6(xy310, xy4010, bb), new_esEs5(xy311, xy4011, bb))
new_esEs16(Nothing, Nothing, bh) → True
new_esEs21(xy301, xy4001, app(ty_[], fb)) → new_esEs5(xy301, xy4001, fb)
new_esEs11(xy30, xy400) → new_primEqInt(xy30, xy400)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_@2, bdh), bea)) → new_esEs14(xy300, xy4000, bdh, bea)
new_esEs6(xy310, xy4010, ty_Ordering) → new_esEs8(xy310, xy4010)
new_esEs5([], :(xy4010, xy4011), bb) → False
new_esEs5(:(xy310, xy311), [], bb) → False
new_esEs4(xy30, xy400, ty_Ordering) → new_esEs8(xy30, xy400)
new_esEs6(xy310, xy4010, app(app(ty_@2, bf), bg)) → new_esEs14(xy310, xy4010, bf, bg)
new_esEs22(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs20(xy300, xy4000, app(app(ty_@2, ec), ed)) → new_esEs14(xy300, xy4000, ec, ed)
new_primPlusNat0(Zero, xy400100) → Succ(xy400100)
new_esEs20(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Maybe, ee)) → new_esEs16(xy300, xy4000, ee)
new_esEs13(Left(xy300), Left(xy4000), ty_Ordering, be) → new_esEs8(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_sr(Pos(xy3010), Neg(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_sr(Neg(xy3010), Pos(xy40010)) → Neg(new_primMulNat0(xy3010, xy40010))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_@0, be) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(ty_Either, bd), be)) → new_esEs13(xy310, xy4010, bd, be)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Maybe, dc)) → new_esEs16(xy300, xy4000, dc)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(app(ty_@3, bed), bee), bef)) → new_esEs18(xy300, xy4000, bed, bee, bef)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Left(xy300), Left(xy4000), ty_Char, be) → new_esEs9(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Double) → new_esEs19(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), app(app(app(ty_@3, de), df), dg)) → new_esEs18(xy300, xy4000, de, df, dg)
new_esEs23(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs20(xy300, xy4000, app(app(ty_Either, ea), eb)) → new_esEs13(xy300, xy4000, ea, eb)
new_esEs12(@0, @0) → True
new_esEs6(xy310, xy4010, ty_Double) → new_esEs19(xy310, xy4010)
new_esEs22(xy300, xy4000, app(app(ty_Either, gf), gg)) → new_esEs13(xy300, xy4000, gf, gg)
new_esEs22(xy300, xy4000, ty_Integer) → new_esEs10(xy300, xy4000)
new_esEs4(xy30, xy400, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy30, xy400, cb, cc, cd)
new_esEs24(xy302, xy4002, ty_Bool) → new_esEs15(xy302, xy4002)
new_primEqNat0(Succ(xy3000), Zero) → False
new_primEqNat0(Zero, Succ(xy40000)) → False
new_esEs4(xy30, xy400, app(ty_[], bc)) → new_esEs5(xy30, xy400, bc)
new_esEs23(xy301, xy4001, app(app(app(ty_@3, baf), bag), bah)) → new_esEs18(xy301, xy4001, baf, bag, bah)
new_esEs20(xy300, xy4000, app(ty_[], dh)) → new_esEs5(xy300, xy4000, dh)
new_esEs22(xy300, xy4000, app(app(ty_@2, gh), ha)) → new_esEs14(xy300, xy4000, gh, ha)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs13(Left(xy300), Left(xy4000), app(app(ty_@2, bcf), bcg), be) → new_esEs14(xy300, xy4000, bcf, bcg)
new_esEs16(Just(xy300), Just(xy4000), ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(ty_@2, ff), fg)) → new_esEs14(xy301, xy4001, ff, fg)
new_esEs10(Integer(xy300), Integer(xy4000)) → new_primEqInt(xy300, xy4000)
new_esEs15(False, True) → False
new_esEs15(True, False) → False
new_esEs23(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs14(@2(xy300, xy301), @2(xy4000, xy4001), bf, bg) → new_asAs(new_esEs20(xy300, xy4000, bf), new_esEs21(xy301, xy4001, bg))
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs24(xy302, xy4002, ty_Double) → new_esEs19(xy302, xy4002)
new_esEs24(xy302, xy4002, app(app(ty_@2, bbd), bbe)) → new_esEs14(xy302, xy4002, bbd, bbe)
new_esEs26(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs22(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_[], hg)) → new_esEs5(xy301, xy4001, hg)
new_esEs4(xy30, xy400, ty_Char) → new_esEs9(xy30, xy400)
new_esEs16(Just(xy300), Just(xy4000), ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs23(xy301, xy4001, app(ty_Ratio, bae)) → new_esEs17(xy301, xy4001, bae)
new_esEs22(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs20(xy300, xy4000, app(ty_Ratio, ef)) → new_esEs17(xy300, xy4000, ef)
new_esEs13(Left(xy300), Left(xy4000), ty_Double, be) → new_esEs19(xy300, xy4000)
new_esEs4(xy30, xy400, ty_Int) → new_esEs11(xy30, xy400)
new_esEs24(xy302, xy4002, ty_Int) → new_esEs11(xy302, xy4002)
new_esEs22(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs4(xy30, xy400, app(ty_Ratio, ca)) → new_esEs17(xy30, xy400, ca)
new_esEs4(xy30, xy400, ty_Float) → new_esEs7(xy30, xy400)
new_esEs20(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs19(Double(xy300, xy301), Double(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_esEs21(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(app(app(ty_@3, bdb), bdc), bdd), be) → new_esEs18(xy300, xy4000, bdb, bdc, bdd)
new_esEs22(xy300, xy4000, app(ty_[], ge)) → new_esEs5(xy300, xy4000, ge)
new_esEs8(LT, LT) → True
new_esEs16(Just(xy300), Just(xy4000), ty_@0) → new_esEs12(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs23(xy301, xy4001, ty_Double) → new_esEs19(xy301, xy4001)
new_esEs21(xy301, xy4001, app(app(app(ty_@3, gb), gc), gd)) → new_esEs18(xy301, xy4001, gb, gc, gd)
new_sr(Neg(xy3010), Neg(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_asAs(False, xy31) → False
new_sr(Pos(xy3010), Pos(xy40010)) → Pos(new_primMulNat0(xy3010, xy40010))
new_esEs16(Just(xy300), Just(xy4000), ty_Ordering) → new_esEs8(xy300, xy4000)
new_primEqNat0(Zero, Zero) → True
new_esEs20(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_primMulNat0(Succ(xy30100), Zero) → Zero
new_primMulNat0(Zero, Succ(xy400100)) → Zero
new_esEs16(Just(xy300), Just(xy4000), ty_Float) → new_esEs7(xy300, xy4000)
new_esEs21(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), ty_Integer, be) → new_esEs10(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_@0) → new_esEs12(xy310, xy4010)
new_esEs18(@3(xy300, xy301, xy302), @3(xy4000, xy4001, xy4002), cb, cc, cd) → new_asAs(new_esEs22(xy300, xy4000, cb), new_asAs(new_esEs23(xy301, xy4001, cc), new_esEs24(xy302, xy4002, cd)))
new_esEs24(xy302, xy4002, app(ty_Ratio, bbg)) → new_esEs17(xy302, xy4002, bbg)
new_esEs24(xy302, xy4002, app(ty_Maybe, bbf)) → new_esEs16(xy302, xy4002, bbf)
new_esEs13(Left(xy300), Left(xy4000), ty_Int, be) → new_esEs11(xy300, xy4000)
new_esEs6(xy310, xy4010, app(ty_Ratio, ca)) → new_esEs17(xy310, xy4010, ca)
new_esEs6(xy310, xy4010, ty_Bool) → new_esEs15(xy310, xy4010)
new_esEs13(Left(xy300), Left(xy4000), app(ty_[], bcc), be) → new_esEs5(xy300, xy4000, bcc)
new_esEs23(xy301, xy4001, ty_Char) → new_esEs9(xy301, xy4001)
new_esEs4(xy30, xy400, ty_@0) → new_esEs12(xy30, xy400)
new_esEs8(GT, GT) → True
new_esEs24(xy302, xy4002, app(ty_[], bba)) → new_esEs5(xy302, xy4002, bba)
new_primPlusNat0(Succ(xy320), xy400100) → Succ(Succ(new_primPlusNat1(xy320, xy400100)))
new_esEs24(xy302, xy4002, ty_Integer) → new_esEs10(xy302, xy4002)
new_esEs13(Right(xy300), Right(xy4000), bd, app(ty_Maybe, beb)) → new_esEs16(xy300, xy4000, beb)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs23(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs4(xy30, xy400, ty_Integer) → new_esEs10(xy30, xy400)
new_esEs22(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs6(xy310, xy4010, ty_Char) → new_esEs9(xy310, xy4010)
new_esEs23(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_primEqInt(Neg(Succ(xy3000)), Neg(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Left(xy4000), bd, be) → False
new_esEs13(Left(xy300), Right(xy4000), bd, be) → False
new_esEs15(True, True) → True
new_esEs20(xy300, xy4000, ty_Ordering) → new_esEs8(xy300, xy4000)
new_esEs13(Right(xy300), Right(xy4000), bd, app(app(ty_Either, bdf), bdg)) → new_esEs13(xy300, xy4000, bdf, bdg)
new_esEs23(xy301, xy4001, ty_Ordering) → new_esEs8(xy301, xy4001)
new_primPlusNat1(Zero, Succ(xy4001000)) → Succ(xy4001000)
new_primPlusNat1(Succ(xy3200), Zero) → Succ(xy3200)
new_esEs23(xy301, xy4001, app(ty_Maybe, bad)) → new_esEs16(xy301, xy4001, bad)
new_esEs4(xy30, xy400, ty_Bool) → new_esEs15(xy30, xy400)
new_esEs21(xy301, xy4001, ty_Float) → new_esEs7(xy301, xy4001)
new_esEs16(Just(xy300), Just(xy4000), app(app(ty_@2, da), db)) → new_esEs14(xy300, xy4000, da, db)
new_esEs7(Float(xy300, xy301), Float(xy4000, xy4001)) → new_esEs11(new_sr(xy300, xy4000), new_sr(xy301, xy4001))
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs4(xy30, xy400, app(app(ty_Either, bd), be)) → new_esEs13(xy30, xy400, bd, be)
new_esEs16(Nothing, Just(xy4000), bh) → False
new_esEs16(Just(xy300), Nothing, bh) → False
new_primEqInt(Neg(Zero), Neg(Succ(xy40000))) → False
new_primEqInt(Neg(Succ(xy3000)), Neg(Zero)) → False
new_esEs13(Left(xy300), Left(xy4000), ty_Bool, be) → new_esEs15(xy300, xy4000)
new_esEs8(EQ, EQ) → True
new_esEs20(xy300, xy4000, ty_Bool) → new_esEs15(xy300, xy4000)
new_esEs24(xy302, xy4002, app(app(ty_Either, bbb), bbc)) → new_esEs13(xy302, xy4002, bbb, bbc)
new_esEs22(xy300, xy4000, app(ty_Ratio, hc)) → new_esEs17(xy300, xy4000, hc)
new_esEs9(Char(xy300), Char(xy4000)) → new_primEqNat0(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Int) → new_esEs11(xy300, xy4000)
new_esEs21(xy301, xy4001, app(app(ty_Either, fc), fd)) → new_esEs13(xy301, xy4001, fc, fd)
new_esEs16(Just(xy300), Just(xy4000), app(ty_[], ce)) → new_esEs5(xy300, xy4000, ce)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs20(xy300, xy4000, ty_Char) → new_esEs9(xy300, xy4000)
new_esEs21(xy301, xy4001, app(ty_Ratio, ga)) → new_esEs17(xy301, xy4001, ga)
new_asAs(True, xy31) → xy31
new_esEs13(Right(xy300), Right(xy4000), bd, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs16(Just(xy300), Just(xy4000), ty_Double) → new_esEs19(xy300, xy4000)
new_esEs25(xy300, xy4000, ty_Int) → new_esEs11(xy300, xy4000)
new_esEs22(xy300, xy4000, app(ty_Maybe, hb)) → new_esEs16(xy300, xy4000, hb)
new_primMulNat0(Succ(xy30100), Succ(xy400100)) → new_primPlusNat0(new_primMulNat0(xy30100, Succ(xy400100)), xy400100)
new_primEqInt(Pos(Succ(xy3000)), Pos(Succ(xy40000))) → new_primEqNat0(xy3000, xy40000)
new_esEs26(xy301, xy4001, ty_Integer) → new_esEs10(xy301, xy4001)
new_esEs13(Left(xy300), Left(xy4000), app(ty_Ratio, bda), be) → new_esEs17(xy300, xy4000, bda)
new_esEs22(xy300, xy4000, ty_Double) → new_esEs19(xy300, xy4000)
new_esEs20(xy300, xy4000, ty_@0) → new_esEs12(xy300, xy4000)
new_esEs6(xy310, xy4010, app(app(app(ty_@3, cb), cc), cd)) → new_esEs18(xy310, xy4010, cb, cc, cd)
new_primEqNat0(Succ(xy3000), Succ(xy40000)) → new_primEqNat0(xy3000, xy40000)
new_esEs4(xy30, xy400, app(ty_Maybe, bh)) → new_esEs16(xy30, xy400, bh)
new_esEs6(xy310, xy4010, app(ty_[], bc)) → new_esEs5(xy310, xy4010, bc)
new_esEs16(Just(xy300), Just(xy4000), app(ty_Ratio, dd)) → new_esEs17(xy300, xy4000, dd)
new_esEs23(xy301, xy4001, app(app(ty_@2, bab), bac)) → new_esEs14(xy301, xy4001, bab, bac)
new_esEs24(xy302, xy4002, ty_Ordering) → new_esEs8(xy302, xy4002)
new_esEs24(xy302, xy4002, ty_Float) → new_esEs7(xy302, xy4002)
new_esEs23(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_esEs21(xy301, xy4001, ty_Int) → new_esEs11(xy301, xy4001)
new_esEs4(xy30, xy400, app(app(ty_@2, bf), bg)) → new_esEs14(xy30, xy400, bf, bg)
new_esEs13(Left(xy300), Left(xy4000), ty_Float, be) → new_esEs7(xy300, xy4000)
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xy40000))) → False
new_primEqInt(Pos(Succ(xy3000)), Pos(Zero)) → False
new_esEs22(xy300, xy4000, ty_Float) → new_esEs7(xy300, xy4000)
new_esEs17(:%(xy300, xy301), :%(xy4000, xy4001), ca) → new_asAs(new_esEs25(xy300, xy4000, ca), new_esEs26(xy301, xy4001, ca))
new_esEs24(xy302, xy4002, ty_@0) → new_esEs12(xy302, xy4002)
new_esEs21(xy301, xy4001, ty_Bool) → new_esEs15(xy301, xy4001)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs21(xy301, xy4001, ty_@0) → new_esEs12(xy301, xy4001)
new_esEs22(xy300, xy4000, app(app(app(ty_@3, hd), he), hf)) → new_esEs18(xy300, xy4000, hd, he, hf)
new_esEs20(xy300, xy4000, app(app(app(ty_@3, eg), eh), fa)) → new_esEs18(xy300, xy4000, eg, eh, fa)
new_esEs15(False, False) → True
The set Q consists of the following terms:
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5([], [], x0)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Double)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(False, True)
new_esEs15(True, False)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(True, True)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(Just(x0), Nothing, x1)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(False, False)
new_esEs8(GT, GT)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs7(Float(x0, x1), Float(x2, x3))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(LT, LT)
new_esEs22(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs10(Integer(x0), Integer(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs6(x0, x1, ty_Int)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs6(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Float)
new_esEs16(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_asAs(True, x0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs6(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs6(x0, x1, ty_Char)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(:(x0, x1), [], x2)
new_esEs6(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs17(:%(x0, x1), :%(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_Char)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(xy400, xy401), xy41), bb) → new_deleteBy([], xy41, bb)
R is empty.
The set Q consists of the following terms:
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5([], [], x0)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Double)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(False, True)
new_esEs15(True, False)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(True, True)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(Just(x0), Nothing, x1)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(False, False)
new_esEs8(GT, GT)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs7(Float(x0, x1), Float(x2, x3))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(LT, LT)
new_esEs22(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs10(Integer(x0), Integer(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs6(x0, x1, ty_Int)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs6(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Float)
new_esEs16(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_asAs(True, x0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs6(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs6(x0, x1, ty_Char)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(:(x0, x1), [], x2)
new_esEs6(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs17(:%(x0, x1), :%(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_Char)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Int)
new_esEs21(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs5([], [], x0)
new_esEs13(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs6(x0, x1, ty_Integer)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Double)
new_esEs13(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(False, True)
new_esEs15(True, False)
new_esEs8(EQ, EQ)
new_primPlusNat1(Succ(x0), Zero)
new_esEs15(True, True)
new_esEs13(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5([], :(x0, x1), x2)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_Double)
new_esEs4(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Double)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs16(Just(x0), Nothing, x1)
new_esEs13(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs15(False, False)
new_esEs8(GT, GT)
new_esEs6(x0, x1, app(ty_Maybe, x2))
new_esEs13(Left(x0), Left(x1), ty_Int, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs7(Float(x0, x1), Float(x2, x3))
new_esEs13(Left(x0), Left(x1), ty_@0, x2)
new_primPlusNat0(Zero, x0)
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(LT, LT)
new_esEs22(x0, x1, ty_Float)
new_esEs13(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Float)
new_esEs6(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs10(Integer(x0), Integer(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), ty_Char, x2)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs6(x0, x1, app(ty_[], x2))
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs25(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Ordering)
new_primEqNat0(Zero, Zero)
new_esEs4(x0, x1, ty_Float)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs6(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs13(Left(x0), Right(x1), x2, x3)
new_esEs13(Right(x0), Left(x1), x2, x3)
new_esEs24(x0, x1, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs12(@0, @0)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs21(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Bool)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs13(Right(x0), Right(x1), x2, ty_Char)
new_esEs6(x0, x1, ty_Int)
new_esEs6(x0, x1, app(ty_Ratio, x2))
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs6(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_@0)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(:(x0, x1), :(x2, x3), x4)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs6(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs22(x0, x1, ty_Double)
new_esEs24(x0, x1, ty_Ordering)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, ty_Char)
new_primMulNat0(Zero, Succ(x0))
new_asAs(False, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs13(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs13(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs13(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs23(x0, x1, ty_Float)
new_esEs16(Nothing, Nothing, x0)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_Bool)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, Zero)
new_asAs(True, x0)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs6(x0, x1, ty_@0)
new_esEs13(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Left(x0), Left(x1), ty_Bool, x2)
new_esEs13(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs14(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs13(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Int)
new_esEs6(x0, x1, ty_Char)
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs5(:(x0, x1), [], x2)
new_esEs6(x0, x1, ty_Bool)
new_esEs13(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(Char(x0), Char(x1))
new_esEs6(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs11(x0, x1)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs6(x0, x1, ty_Ordering)
new_esEs13(Left(x0), Left(x1), ty_Integer, x2)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs17(:%(x0, x1), :%(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs20(x0, x1, ty_Double)
new_esEs16(Just(x0), Just(x1), ty_Char)
↳ HASKELL
↳ IFR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_deleteBy([], :(:(xy400, xy401), xy41), bb) → new_deleteBy([], xy41, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_deleteBy([], :(:(xy400, xy401), xy41), bb) → new_deleteBy([], xy41, bb)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3